r:CRng, p:Ideal(r){i}. (u:|r|. Dec(p(u)))  SqStable(IsPrimeIdeal(r;p)) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, Ideal(r){i}, IsPrimeIdeal(R;P)
Definitions	, t  T, P  Q, x:A. B(x), x. t(x), P  Q, x f y, IsPrimeIdeal(R;P), Rng, Ideal(r){i}, CRng, x(s)
Lemmas	crng wf, ideal wf, decidable wf, rng car wf, decidable or, sq stable from decidable, sq stable all, sq stable not, rng times wf, rng one wf, not wf, sq stable and